\section{Определенность переменных}

Множество множеств переменных: $D=2^X$.

\begin{itemize}
  \item Семантика выражений: $\sembr{\bullet}:{\cal E}\to(D\to\{\term{Ok},\term{Oops}\})$.
        $$\sembr{n}=\lambda d.\term{Ok}$$
        $$
           \sembr{x}=\lambda d.\left\{
                                  \begin{array}{rcl}
                                     \term{Ok}&,&x\in d\\
                                     \term{Oops}&,&\mbox{иначе}
                                  \end{array}
                               \right.
        $$
        $$
           \sembr{A\otimes B}=\lambda d.\left\{
                                  \begin{array}{rcl}
                                     \term{Ok}&,&\sembr{A}\;d=\term{Ok}\mbox{ и }\sembr{B}\;d=\term{Ok}\\
                                     \term{Oops}&,&\mbox{иначе}
                                  \end{array}
                               \right.
        $$
  \item Семантика операторов:

    $$
      \trans{d}{\llang{skip}}{d}
    $$

    $$
      \ctrans{d}{\llang{$x\;$:=$\;e$}}{d\cup\{x\}}{\sembr{e}\;d=\term{Ok}}
    $$

    $$
      \trans{d}{\llang{read$\;x$}}{d\cup\{x\}}
    $$

    $$
      \ctrans{d}{\llang{write$\;e$}}{d}{\sembr{e}\;d=\term{Ok}}
    $$

    $$
      \trule{\trans{d}{\llang{$S_1$}}{d^\prime},\;\trans{d^\prime}{\llang{$S_2$}}{d^{\prime\prime}}}
            {\trans{d}{\llang{$S_1\;$;$\;S_2$}}{d^{\prime\prime}}}
    $$

    $$
      \crule{\trans{d}{\llang{$S_1$}}{d^\prime},\;\trans{d}{\llang{$S_2$}}{d^{\prime\prime}}}
            {\trans{d}{\llang{if$\;e\;$then$\;S_1\;$else$\;S_2$}}{d^\prime\cap d^{\prime\prime}}}
            {\sembr{e}\;d=\term{Ok}}
    $$

    $$
      \crule{\trans{d}{\llang{$S$}}{d^\prime}}
            {\trans{d}{\llang{while$\;e\;$do$\;S$}}{d}}
            {\sembr{e}\;d=\term{Ok}}
    $$

  \item Семантика программ: $\sembr{\bullet}_P:{\cal P}\to\{\term{Ok},\term{Oops}\}$

        $$
          \sembr{P}_p=\left\{
                         \begin{array}{rcl}
                            \term{Ok}&,&\exists d\in D\;:\;\trans{\emptyset}{\llang{$P$}}{d}\\
                            \term{Oops}&,&\mbox{ иначе}
                         \end{array}
                      \right.
        $$
\end{itemize}


